frame-p(es; i; T; x; L)
== subtype_rel(es-vartype(es; i; x); T)
== c alle-at(es;
== c alle-at(i;
== c alle-at(e.(((es-kind(es; e)  L))
== c alle-at( (t:rationals. es_state_after(es; e)(x,t) = es_state_when(es; e)(x,t)))) 

latex

---

clarification:

frame-p(es; i; T; x; L)
== subtype_rel(es-vartype(es; i; x); T)
== c alle-at(es;
== c alle-at(i;
== c alle-at(e.(((es-kind(es; e)  L  Knd))
== c alle-at( (t:rationals. es_state_after(es; e)(x,t) = es_state_when(es; e)(x,t)  T))) 

latex

Definitions	A c B, es-vartype(es; i; x), alle-at(es; i; e.P(e)), P  Q, A, (x  l), es-kind(es; e), Knd, x:A. B(x), rationals, s = t, es_state_after(es; e), f(a), es_state_when(es; e)
FDL editor aliases	frame-p